#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"
int lib(int n){
    if(klee_change(0,1)){
        if(n > 0){
            int acc = 1;
            int x = 1;
            while(x < n + 1){
                acc = acc * x;
                x = x +1;
            }
            return acc;
        }
        return 0;
    }
    else{
        if(n <= 0){
            return 0;
        }else if(n ==1){
            return 1;
        }else{
            return n * lib(n-1);
        }
    }
}

int factorial(int x){
    if(x<5){
        return lib(x);
    }else{
        return 0;
    }
}
int main(int argc, char *argv[]) {
  int x= argv[1][0] - '0';
  return factorial(x);
}
